When the decreasing parameter is a named parameter to the function, it can be specified by referring to its name.

When the decreasing parameter is not named in the signature, a name can be introduced locally in the Lean.Parser.Command.declaration : commandtermination_by clause.

The decreasing parameter's type must be an inductive type. In notInductive, a function is specified as the decreasing parameter:

cannot use specified measure for structural recursion:
  its type is not an inductive

If the decreasing parameter is an indexed family, all the indices must be variables. In constantIndex, the indexed family Fin' is instead applied to a constant value:

cannot use specified measure for structural recursion:
  its type Fin' is an inductive family and indices are not variables
    Fin' 100

The parameters of the decreasing parameter's type must not depend on function parameters that come after varying parameters or indices. In afterVarying, the fixed prefix is empty, because the first parameter n varies, so p is not part of the fixed prefix:

failed to infer structural recursion:
Cannot use parameter x:
  failed to eliminate recursive application
    afterVarying (n + 1) p WithParam'.zero

In the following example, the decreasing parameter n is matched against the nested pattern .succ (.succ n). Therefore .succ (.succ n) is a (non-strict) sub-term of n, and consequently both n and .succ n are strict sub-terms, and the definition is accepted.

For clarity, this example uses .succ n and .succ (.succ n) instead of the equivalent Nat-specific n+1 and n+2.

In the following example, the decreasing parameter n is not directly the discriminant of the Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not. match expression. Therefore, n' is not considered a sub-term of n.

failed to infer structural recursion:
Cannot use parameter n:
  failed to eliminate recursive application
    half n'

Using well-founded recursion, and explicitly connecting the discriminant to the pattern of the match, this definition can be accepted.

Similarly, the following example fails: although xs.tail would reduce to a strict sub-term of xs, this is not visible to Lean according to the rules above. In particular, xs.tail is not definitionally equal to a strict sub-term of xs.

An important consequence of the strategies that are used to prove termination is that simultaneous matching of two discriminants is not equivalent to matching a pair. Simultaneous matching maintains the connection between the discriminants and the patterns, allowing the pattern matching to refine the types of the assumptions in the local context as well as the expected type of the Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not. match. Essentially, the elaboration rules for Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not. match treat the discriminants specially, and changing discriminants in a way that preserves the run-time meaning of a program does not necessarily preserve the compile-time meaning.

This function that finds the minimum of two natural numbers is defined by structural recursion on its first parameter:

Replacing the simultaneous pattern match on both parameters with a match on a pair causes termination analysis to fail:

failed to infer structural recursion:
Cannot use parameter n:
  failed to eliminate recursive application
    min' n' k'

This is because the analysis only considers direct pattern matching on parameters when matching recursive calls to strictly-smaller argument values. Wrapping the discriminants in a pair breaks the connection.

This function that finds the minimum of the two components of a pair can't be elaborated via structural recursion.

failed to infer structural recursion:
Cannot use parameter nk:
  the type Nat × Nat does not have a `.brecOn` recursor

This is because the parameter's type, Prod, is not recursive. Thus, its constructor has no recursive parameters that can be exposed by pattern matching.

This definition is accepted using well-founded recursion, however:

Even though the recursive occurrence of countdown is applied to a term that is not a strict sub-term of the decreasing parameter, the following definition is accepted:

This is because n' + 0 is definitionally equal to n', which is a strict sub-term of n. Sub-terms that result from pattern matching are connected to the discriminant using the rules for match generalization, which respect definitional equality.

In countdown', the recursive occurrence is applied to 0 + n', which is not definitionally equal to n' because addition on natural numbers is structurally recursive in its second parameter:

failed to infer structural recursion:
Cannot use parameter n:
  failed to eliminate recursive application
    countdown' (0 + n')

The following example demonstrates mutual recursion over a non-mutual inductive data type:

The following example demonstrates recursion over mutually inductive types. The functions Exp.size and App.size are mutually recursive.

The definition of App.numArgs is structurally recursive over type App. It demonstrates that not all inductive types in the mutual group need to be handled.

Lean automatically infers that the function half is structurally recursive. The termination_by? clause causes the inferred termination annotation to be displayed, and it can be automatically added to the source file with a single click.

Try this: termination_by structural x => x

Addition of natural numbers can be defined via recursion on the second argument. This function is straightforwardly structurally recursive.

Defined using Nat.rec, it is much further from the notations that most people are used to.

Structural recursive calls made on data that isn't the immediate child of the function parameter requires either creativity or a complex yet systematic encoding.

One way to think about this function is as a structural recursion that flips a bit at each call, only incrementing the result when the bit is set.

[0, 0, 1, 1, 2, 2, 3, 3, 4]

Instead of creativity, a general technique called course-of-values recursion can be used. Course-of-values recursion uses helpers that can be systematically derived for every inductive type, defined in terms of the recursor; Lean derives them automatically. For every Nat n, the type n.below (motive := mot) provides a value of type mot k for all k < n, represented as an iterated dependent pair type. The course-of-values recursor Nat.brecOn allows a function to use the result for any smaller Nat. Using it to define the function is inconvenient:

The function is marked Lean.Parser.Command.declaration : commandnoncomputable because the compiler doesn't support generating code for course-of-values recursion, which is intended for reasoning rather that efficient code. The kernel can still be used to test the function, however:

[0, 0, 1, 1, 2, 2, 3, 3, 4]

The dependent pattern matching in the body of half'' can also be encoded using recursors (specifically, Nat.casesOn), if necessary:

This definition still works.

[0, 0, 1, 1, 2, 2, 3, 3, 4]

However, it is now far from the original definition and it has become difficult for most people to understand. Recursors are an excellent logical foundation, but not an easy way to write programs or proofs.

This definition is equivalent to List.below:

In other words, for a given motive, List.below' is a type that contains a realization of the motive for all suffixes of the list.

More recursive arguments require further nested iterations of the product type. For instance, binary trees have two recursive occurrences.

Its corresponding course-of-values table contains the realizations of the motive for all subtrees:

For both lists and trees, the brecOn operator expects just a single case, rather than one per constructor. This case accepts a list or tree along with a table of results for all smaller values; from this, it should satisfy the motive for the provided value. Dependent case analysis of the provided value automatically refines the type of the memo table, providing everything needed.

The following definitions are equivalent to List.brecOn and Tree.brecOn, respectively. The primitive recursive helpers List.brecOnTable and Tree.brecOnTable compute the course-of-values tables along with the final results, and the actual definitions of the brecOn operators simply project out the result.

The first step in walking through the elaboration of half is to manually desugar it to a simpler form. This doesn't match the way Lean works, but its output is much easier to read when there are fewer OfNat instances present. This readable definition:

can be rewritten to this somewhat lower-level version:

The elaborator begins by elaborating a pre-definition in which recursion is still present but the definition is otherwise in Lean's core type theory. Turning on the compiler's tracing of pre-definitions, as well as making the pretty printer more explicit, makes the resulting pre-definition visible:

The returned trace message is:

[Elab.definition.body] half : Nat → Nat :=
    fun (x : Nat) =>
      half.match_1.{1} (fun (x : Nat) => Nat) x
        (fun (_ : Unit) => Nat.zero)
        (fun (_ : Unit) => Nat.zero)
        fun (n : Nat) => Nat.succ (half n)

The auxiliary match function's definition is:

def half.match_1.{u_1} : (motive : Nat → Sort u_1) →
  (x : Nat) → (Unit → motive Nat.zero) → (Unit → motive 1) → ((n : Nat) → motive n.succ.succ) → motive x :=
fun motive x h_1 h_2 h_3 => Nat.casesOn x (h_1 ()) fun n => Nat.casesOn n (h_2 ()) fun n => h_3 n

Formatted more readably, this definition is:

In other words, the specific configuration of patterns used in half are captured in half.match_1.

This definition is a more readable version of half's pre-definition:

To elaborate it as a structurally recursive function, the first step is to establish the bRecOn invocation. The definition must be marked Lean.Parser.Command.declaration : commandnoncomputable because Lean does not support code generation for recursors such as Nat.brecOn.

The next step is to replace occurrences of x in the original function body with the n provided by brecOn. Because table's type depends on x, it must also be generalized when splitting cases with half.match_1, leading to a motive with an extra parameter.

The three cases' placeholders expect the following types:

don't know how to synthesize placeholder for argument 'h_1'
context:
x n : Nat
table : Nat.below n
⊢ Unit → (fun k => Nat.below k → Nat) Nat.zero

don't know how to synthesize placeholder for argument 'h_2'
context:
x n : Nat
table : Nat.below n
⊢ Unit → (fun k => Nat.below k → Nat) 1

don't know how to synthesize placeholder for argument 'h_3'
context:
x n : Nat
table : Nat.below n
⊢ (n : Nat) → (fun k => Nat.below k → Nat) n.succ.succ

The first two cases in the pre-definition are constant functions, with no recursion to check:

The final case contains a recursive call. It should be translated into a lookup into the course-of-values table. A more readable representation of the last hole's type is:

which is equivalent to

The first Nat in the course-of-values table is the result of recursion on n + 1, and the second is the result of recursion on n. The recursive call can thus be replaced by a lookup, and the elaboration is successful:

The actual elaborator keeps track of the relationship between the parameter being checked for structural recursion and the positions in the course-of-values tables by inserting sentinel types with fresh names into the motive.

Function types in general do not have a well-founded relation that's useful for termination proofs. Instance synthesis thus selects instSizeOfDefault and the corresponding well-founded relation. If the measure is a function, the default SizeOf instance is selected and the proof cannot succeed.

The following recursive definition of the Fibonacci numbers has two recursive calls, which results in two goals in the termination proof.

Here, the measure is simply the parameter itself, and the well-founded order is the less-than relation on natural numbers. The first proof goal requires the user to prove that the argument of the first recursive call, namely n - 1, is strictly smaller than the function's parameter, n.

Both termination proofs can be easily discharged using the omega tactic.

If a parameter of the function is the discriminant of a pattern match, then the proof obligations mention the refined parameter.

Here, the termIfThenElse : term`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to return `t` or `e` depending on whether `c` is true or false. The explicit argument `c : Prop` does not have any actual computational content, but there is an additional `[Decidable c]` argument synthesized by typeclass inference which actually determines how to evaluate `c` to true or false. Write `if h : c then t else e` instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact that `c` is true/false. if does not add a local assumption about the condition (that is, whether n ≤ 1) to the local contexts in the branches.

Nevertheless, the assumptions are available in the context of the termination proof:

Termination proof obligations in body of a Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. `for x in e, x2 in e2, ... do s` iterates of the given collections in parallel, until at least one of them is exhausted. The types of `e2` etc. must implement the `ToStream` typeclass. for​…​Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. `for x in e, x2 in e2, ... do s` iterates of the given collections in parallel, until at least one of them is exhausted. The types of `e2` etc. must implement the `ToStream` typeclass. in loop are also enriched, in this case with a Std.Range membership hypothesis:

Similarly, in the following (contrived) example, the termination proof contains an additional assumption showing that x ∈ xs.

This feature requires special setup for the higher-order function under which the recursive call is nested, as described in the section on preprocessing. In the following definition, identical to the one above except using a custom, equivalent function instead of List.map, the proof obligation context is not enriched:

A classic example of a recursive function that needs a more complex measure is the Ackermann function:

The measure is a tuple, so every recursive call has to be on arguments that are lexicographically smaller than the parameters. The default decreasing_tactic can handle this.

In particular, note that the third recursive call has a second argument that is smaller than the second parameter and a first argument that is definitionally equal to the first parameter. This allowed decreasing_tactic to apply Prod.Lex.right.

It fails, however, with the following modified function definition, where the third recursive call's first argument is provably smaller or equal to the first parameter, but not syntactically equal:

failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
case h
m n : Nat
⊢ m / 2 + 1 < m + 1

Because Prod.Lex.right is not applicable, the tactic used Prod.Lex.left, which resulted in the unprovable goal above.

This function definition may require a manual proof that uses the more general theorem Prod.Lex.right', which allows the first component of the tuple (which must be of type Nat) to be less or equal instead of strictly equal: